Nuprl Lemma : p-lift_wf
11,40
postcript
pdf
A
,
B
:Type,
P
:(
A
),
d
:(
x
:
A
Dec(
P
(
x
))),
f
:({
x
:
A
|
P
(
x
)}
B
). p-lift(
d
;
f
)
A
(
B
+ Top)
latex
ProofTree
Definitions
p-lift(
d
;
f
)
,
x
.
A
(
x
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
inl
x
,
inr
x
,
False
,
P
Q
,
left
+
right
,
A
,
Top
,
x
:
A
.
B
(
x
)
,
Void
,
{
x
:
A
|
B
(
x
)}
,
Dec(
P
)
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
f
(
a
)
,
x
:
A
B
(
x
)
,
,
t
T
,
Type
Lemmas
decidable
wf
,
top
wf
origin
A, B:Type, P:(A
), d:(x:ADec(P(x))), f:({x:A| P(x)} B). p-lift(d;f) 
A(B + Top)
A, B:Type, P:(A), d:(x:ADec(P(x))), f:({x:A| P(x)} B). p-lift(d;f) A(B + Top)
x.A(x)
Q
A
x:A.B(x)x:A. B(x)B(x) T